A:Type, eq:EqDecider(A), f, g:a:A fp Type, a:A. f || g  (f  g(a)?Top r g(a)?Top) 

latex

Definitions	Type, f(x), Top, t  T, x:A. B(x), b, A, b, , s = t, , x.A(x), x. t(x), a:A fp B(a), x:AB(x), x  dom(f), P  Q, x:A  B(x), P & Q, P  Q, Unit, left + right, False, if b then t else f fi , f(x)?z, Void, x:A.B(x), EqDecider(T), f || g, f  g
Lemmas	fpf-ap wf, fpf-compatible wf, fpf wf, deq wf, fpf-join-cap-sq, subtype rel self, fpf-cap wf, top wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, fpf-trivial-subtype-top, bool wf, bnot wf, not wf, assert wf